perm filename SATO.TEX[PRO,JMC] blob
sn#747333 filedate 1984-03-16 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00018 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 \input plain.tex[tex,sys]
C00005 00003 \centerline{\bb Joint US-Japanese Collaboration on Logic and Computer Science}
C00007 00004 \title{Expected Scientific Benefits}
C00009 00005 \title{Information on Previous Professional Visits to Japan}
C00012 00006 \title{Current and Pending Support}
C00014 00007 \title{Project Description}
C00016 00008 \name{McCarthy}
C00018 00009 \name{Feferman}
C00022 00010 \name{Goad}
C00026 00011 \name{Ketonen}
C00028 00012 \name{Weyhrauch and Talcott}
C00046 00013 \title{Biography of McCarthy}
C00065 00014 \title{Biography of Feferman}
C00082 00015 \title{Biography of Goad}
C00086 00016 \title{Biography of Ketonen}
C00094 00017 \title{Biography of Talcott}
C00099 00018 \title{Biography of Weyhrauch}
C00113 ENDMK
C⊗;
\input plain.tex[tex,sys]
\hsize=5in
\hoffset=.75in
\def\nextpage{\vfill\eject}
\def\done{\vfill\end}
\def\linebreak{\break}
\def\CR{\hskip 0pt plus 20in\hbox{}\linebreak}
%font information
\font\bb=amr10 scaled \magstep1 %12pt
\font\cc=amr10 scaled \magstep2 %14pt
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\title#1{\vskip 2pc
\hbox{\bf #1}
\vskip 1pc}
\def\name#1{\vskip 1pc
\hbox{\bf #1}
\vskip .5pc}
\def\hangsiz#1{\setbox 9=\hbox to #1{}}
\def\hang#1#2{\noindent\hangindent \wd9\hbox to \wd9{#1}\strut #2}
\def\data#1#2{\hangsiz{6pc}
\hang{#1}{#2}} %#1→date #2→description
\def\biblio{\vskip 2pc
\noindent Bibliography
\vskip 1pc}
\def\bib#1#2{\hangsiz{3pc}
\hang{\hss [#1]\quad }{#2}} %macros for bibliography
\centerline{\bb Joint US-Japanese Collaboration on Logic and Computer Science}
\title{Project Summary}
\noindent This proposal requests funds for co-operative research on
logic and computer science. The proposed collaboration involves
Professor John McCarthy, Professor Solomon Feferman,
Dr.\ Christopher Goad, Dr.\ Jussi Ketonen, Dr.\ Carolyn Talcott and
Dr.\ Richard Weyhrauch at Stanford
University and Professor Masahiko Sato,
Dr.\ Masami Hagiya,
Dr.\ Susumu Hayashi, Dr.\ Hayao Nakahara,
and Dr. Takafumi Sakurai at Tokyo University and Kyoto University.
The purpose of the proposed collaboration is to advance the mathematical
study of symbolic computation. This is one of the central issues
in basic research in Artificial Intelligence. Significant advances in
this area, especially in understanding the role of logic in mechanised
reasoning and design of computer languages, can have far-reaching
consequences for Artifical Intelligence and Logic in general.
\title{Expected Scientific Benefits}
\noindent The groups
represented have a lot of detailed information to share about how logic
can best be used to prove the properties of programs and
what specific software tools are useful in this endeavor. Their
collective experience in proving properties of programs, in the semantics
of programming languages and in logic make this collaboration an ideal
vehicle to synthesize work of the past few years into a more cohesive
understanding of the interaction between logic and computer science.
\title{Information on Previous Professional Visits to Japan}
\noindent John McCarthy and Richard Weyhrauch have made professional visits
to Japan.
\vskip 12pt
\noindent Summary of visits by John McCarthy
\vskip 6pt
\settabs\+\indent&Research Institute of
Mathematical Sciences, Kyoto\qquad&\cr
\+&Lecture at Central Institute Japan, Tokyo&\cr
\+&Information Processing Development Center, Tokyo&2/2--2/16/67\cr
\smallskip
\+&Visit to Electrotechnical Lab., Tokyo&4/9--4/12/70\cr
\smallskip
\+&JITA Symposium, seminars and lectures, Tokyo&3/13--3/25/72\cr
\smallskip
\+&Research Institute of Mathematical Sciences,&\cr
\+&University of Kyoto, Kyoto&3/28--4/12/75\cr
\smallskip
\+&Attend Conference on Mathematical Aspects&\cr
\+&of Computer science&\cr
\+&and IFIP Working Group 2.1, Kyoto&8/23--8/26/78\cr
\smallskip
\+&Visit Nippon Telephone $\&$ Telegraph Co., Tokyo&\cr
\+&and University of Tsukuba, Ibaragi&8/27--9/12/78\cr
\smallskip
\+&Lectures:&\cr
\+&Research Institute of Mathematical Sciences, Kyoto&5/23--5/24/83\cr
\+&Tokyo&5/24--5/29/83\cr
\+&Kyoto&5/30--6/4/83\cr
\nextpage
\noindent Summary of visits by Richard Weyhrauch
\vskip 6pt
\settabs\+\indent&Research Institute of
Mathematical Sciences, Kyoto\qquad&\cr
\+&Attend 2nd USA JAPAN Conference, Tokyo&10/72\cr
\+&Invited address at Japan Math.\ Society, Kyoto&10/72\cr
\+&Symposium on program verification, Kyoto&10/72\cr
\+&Lectures at Mitsubishi Electric Co.&10/72\cr
\smallskip
\+&Talks:&\cr
\+&Tokyo University, Tokyo&10/7/82\cr
\+&ICOT, Tokyo&10/14/82\cr
\+&University of Tsukuba, Ibaragi&10/16/82\cr
\+&Nippon Telephone $\&$ Telegraph Co., Tokyo&10/22/82\cr
\+&University of Kyoto, Kyoto&10/25--10/27/82\cr
\+&NEC, Tokyo&11/4/82\cr
\title{Current and Pending Support}
\noindent John McCarthy is a Professor of Computer Science at Stanford University.
\medskip
\noindent Solomon Feferman is a Professor of Philosophy and Mathematics
at Stanford University. Feferman is supported by NSF grants MCS-8104869 (current)
and MCS-8405825 (proposed), entitled ``Topics in logic and
the functions of mathematics.''
\medskip
\noindent Dr.\ Goad is currently on a leave of absence from Stanford University,
working in industry.
\medskip
\noindent Dr.\ Ketonen is supported by NSF Grant MCS-8206565, entitled
``Mechanical Theorem Proving and Development of EKL---an Interactive
Proof Checking System (Computer Research).''
\medskip
\noindent Professor McCarthy and Dr.\ Talcott are supported by NSF Grant MCS-8104877,
entitled
``Basic Research in Artificial Intelligence (Computer Research).''
\medskip
\noindent Dr.\ Weyhrauch is supported by NSF Grant MCS-8303142, entitled
``The Mechanization of Formal Reasoning (Computer Research).''
\title{Project Description}
\noindent {\bf US-Japanese cooperative aspects, Scientific Justification
and Objectives of the Visits}
\vskip 12pt
\noindent The ``American side'' of the details of the US-Japanese cooperative
aspects,
along with scientific justifications and objectives
is outlined in the individual sections listed below.
Aside from the exchange of professional ideas by mail or other impersonal
means, the proposed research will require travel arrangements to Japan, as outlined
by the budget section of the proposal.
The mathematical study of symbolic computation and formal reasoning
is a relatively new and
very rapidly growing field. One can talk about an almost exponential
increase in activity---correlating with the current
interest in Artifical Intelligence in general. Much of the basic
``know-how'' is ``folklore'' and has not appeared in
published form. One can therefore expect substantial mutual benefits
from professional discussions on the spot.
\nextpage
\name{McCarthy}
\noindent McCarthy will pursue his study of the relation between
functional programming and logic programming including the problem
of giving logic programming more sophisticated forms of control.
This work meshes well with Sato's Qute system that combines
logic programming with LISP style programming.
It has already resulted in the postponement heuristic developed
originally in connection with a Prolog program for coloring maps
but which is more generally applicable to problems where the
deciding how to achieve some goals should be postponed, because
they can be solved no matter how the other goals are solved.
Other work by McCarthy on map coloring in Prolog led to the
idea of introspective Prolog programs and led Peter Szeredi
to write an introspective Prolog interpreter.
\name{Feferman}
\noindent Feferman proposes to work on relations between the theory of programs,
generalized recursion theory and certain formal systems for constructive
mathematics. The latter are the system $T↓0$ presented in [F1979] and its
variants (such as given in [B1984]) as well as interesting subtheories
(e.g. $FM$ and $FM↓0$ from [F1982]).
$T↓0$ provides a general framework in which all of Bishop-style
constructive mathematics can be directly formalized.
Bishop conceived his
work as a high-level programming language. Programs can be extracted in
principle from his proofs, and in theory from their representation in $T↓0$.
(cf.\ [H1983] and [B1984]). However, the next main step is to examine such
programs for their feasibility (modulo standard feasible sub-routines already
developed in the analysis of algorithms). This will require case studies which
can very profitably be carried out with the group in Stanford and from Japan,
in the context of this proposal.
Secondly, the relation between generalizations of recursion theory to
arbitrary structures as abstract data types---and computation on such
types---is well recognized. In practice, however, one deals with many data types
simultaneously. A theoretical framework for a global generalized recursion theory
is needed to account properly for this situation. The system $T↓0$
provides a formal setting in which this can be done. What is required now
is a corresponding (informal) mathematics and development of such a global
recursion theory.
\vskip 12pt
\noindent References
\hangsiz{4pc}
\hang{[B1984]}{M. Beeson, Proving programs and programming proofs. To appear
in Proc.\ 7th ICLMPS/DUHPS (Salzburg).}
\hang{[F1979]}{S. Feferman, Constructive theory of functions and clesses, in
Logic Colloquium 78 (Mons conference), pp.\ 159--224.}
\hang{[F1982]}{S.Feferman, Inductively presented theories, in Logic
Colloquium 80, pp.\ 95--182.}
\hang{[H1983]}{S. Hayashi, Extracting Lisp programs from constructive proofs,
Pub.\ Res.\ Inst.\ Math.\ Sci., Kyoto University 19, pp.\ 161--191}
\name{Goad}
\noindent Goad's work over the last several years has concerned
the automatic
generation and manipulation of algorithms. Within this field, he has
focused on the problem of devising suitable data types for the
representation of algorithms, and on exploiting the resulting technology
for the manipulation of algorithms in the automatic generation of very
fast special purpose programs for particular application areas. The
application areas considered have been computer graphics and computer
vision.
At first sight, the problem of developing data types for algorithms to be
used in the automatic manipulation of algorithms may appear identical to
the problem of programming language design; in each case the task is to
select a concrete representation (a ``program'') for an abstract entity (an
``algorithm''). However, the kinds of representation which are suitable for
human use are not necessarily adequate for the purposes of automatic
manipulation. In particular, a program usually contains only the minimal
information about an algorithm needed to run it, whereas much more
extensive information may be needed for certain kinds of automatic
manipulation. For example, constructive proofs constitute an alternate
formalism for representing algorithms. Goad showed in his thesis that
useful manipulations could be carried out on proofs which could not be
applied to ordinary programs. Since then, he has applied this and other
non-standard representational formalisms for algorithms to two practical
applications: first, the automatic generation of fast algorithms for
displaying three dimensional objects from arbitrary points of view, and
second, the automatic generation of algorithms for finding three
dimensional objects in digitized TV images (three dimensional computer
vision). In both cases, the shape of the object is given in advance, and
is used to automatically construct a very fast algorithm specialized to
the task of displaying or recognizing that one object. The specialized
algorithms produced in this way have substantially better performance than
their manually constructed counterparts.
\name{Ketonen}
\noindent Ketonen has been working on the development of EKL,
an interactive proof checker in high order predicate calculus.
The emphasis has been on creating a system and a language
which would allow the expression and verification of mathematical
facts in a direct and natural way. The approach taken has been quite
succesful: Ketonen has been able to produce an elegant and eminently
readable proof of
Ramsey's theorem (a non-trivial fact in infinitary combinatorics)
in under 50 lines.
Ramsey's theorem
has been used as a benchmark to test the power
of proof checking systems.
At the same time
EKL is versatile enough to be able to verify the associativity if the LISP
append function in just one line.
The above results are important in that they indicate that
programs previously thought to be too complex for
mechanical verification are now within the reach of sufficiently powerful
proof checking systems.
Ketonen expects his experience in designing proof checkers to
be valuable and mutually enriching in the context of
the Qute project of Sato et al.
\name{Weyhrauch and Talcott}
\noindent The FOL system of Richard Weyhrauch represents one approach
to the problem
representing information about programs in a form that allows reasoning
to be done about their properties.
The FOL system is both a tool for exploring the epistemic part
of AI and a programming system for building knowledge-based systems. The
basic premiss of FOL is that formal methods are relevant to these
problems and the hope of the FOL project is to provide a theory of
how formal methods can be used to solve some of the problems of artificial
intelligence and philosophy.
The FOL system is the realization of the FOL ideas in a computer program.
In the past most of our effort has been devoted to showing that certain
problems of AI and philosophy actually can be dealt with satisfactorily in
this environment.
One of the most useful features of our previous work has been the FOL
evaluator together with the notion of semantic attachments. Semantic
attachments are used to bridge the gap between proving properties objects
and finding out properties of objects by computing them. An example we
frequently use ARITH, an FOL context, in which you can not only prove
facts about numbers but also make new function definitions. The values of
these functions can then be computed by the FOL evaluator by using the
semantic attachments already existing in ARITH. In Aiello and
Weyhrauch[1980] we showed how to translate these function definitions into
LISP code. Thus we could translate back and forth between the two styles
of providing answers -- on the one hand we give an axiomatic description
of how to manipulate arithmetic formulas and on the other hand we used a
completely general ``compiler'' to produce LISP code which we used as
semantic attachments to the same function symbols that we were defining.
This exercise led us to have serious questions about the appropriateness
of the programing language, namely LISP, that we were using to write
semantic attachments. Its inadequacy could be seen because of the
difficulty we had writing such a compiler. The difficulties weren't so
much quantitative as qualitative in the sense that it was completely clear
that such a compiler could be written and when we wrote it and watched it
perform, it worked admirably well, but the mapping between the function
definitions in FOL and the programs in LISP wasn't very easy to describe.
Out of this effort and the FOLISP project of Carolyn Talcott (a project
which used FOL extensively as a theorem proving tool for LISP programs),
we developed an interest in what was an appropriate programing language.
In particular, what would an applicative programing language look like
that would exploit our understanding of the FOL evaluator and
integrate computational and declarative reasoning.
This led to the development of RUM, a simple applicative programming
language, and a theory of computation or more precisely, a recursion
theory that is carefully matched to the kind of evaluator provided by the
old FOL ``eval'' routine. We can then write a bi-directional translator
between programs written in RUM and function definitions written in the
logical system of FOL in such a way that the the soundness of the
translation procedure between the programs and the definitions is provable
as a meta-theorem using the recursion theory of RUM formalized in FOL.
Since we intend to implement the new FOL in RUM (see below), one of the
most important applications of this idea is that the translation of the
RUM code for FOL into logical function definitions will provide a sound
axiomatization of the FOL system itself. This impacts our work on
self-referring systems and is the mechanism by which we intend to carry out
the axiomatization of the meta-theory of FOL.
\vskip 12pt
\noindent Mathematical theory of computation
\vskip 6pt
\noindent Within the FOL framework one can represent programs (from any
language) as
objects. The semantics of a programming language can be expressed in a
number of different ways -- for example, as the function computed by an
applicative program or via structures representing the computation history
defined by a program. Schemes for proving correctness and other
properties can be formulated and used as tools for reasoning. In short we
have the means for formalizing diverse aspects of MTC that are generally
treated in separate systems. One goal of our MTC work is to show how to
take advantage of this power. Although we will concentrate to some degree
on the development and application of the theory of RUM, much of the work
will be directly applicable to other languages. In general it will
provide a paradigm for such applications.
By taking advantage of the richness of FOL we can not only represent
operations on programs, we can also discuss properties of these operations
such as soundness, recursion depth, memory usage, other execution cost
measures, or program size. Thus this serves as another example of the
use of FOL to handle intensional reasoning.
RUM is a subset of a collection of computation theories (and programming
systems) currently being investigated by Carolyn Talcott. The work will
eventually be formalized in FOL and incorporated as tools of FOL.
\nextpage
\title{Biography of McCarthy}
\vskip 12pt
\data{Born:}{September 4, 1927 in Boston, Massachusetts}
\vskip 15pt
\noindent Education:
\data{1948}{B.S. (Mathematics) California Institute of Technology,}
\data{1951}{Ph.D. (Mathematics) Princeton University}
\vskip 15pt
\noindent Honors and Societies:
\data{}{American Academy of Arts and Sciences}
\data{}{American Society for the Advancement of Science}
\data{}{American Mathematical Society}
\data{}{Association for Computing Machinery}
\data{}{IEEE}
\data{}{Sigma Xi}
\data{}{Sloan Fellow in Physical Science, 1957--59}
\data{}{ACM National Lecturer, 1961}
\data{}{A.M. Turing Award from Association for Computing Machinery, 1971}
\data{}{Editorial Board, Artificial Intelligence Journal, 1975--present}
\data{}{Academic Advisor, National Legal Center for Public Information,
1976--present}
\data{}{Board of Directors, Information International, Inc.}
\data{}{Sigma Xi National Lecturer, 1977}
\vskip 15pt
\noindent Professional Record:
\vskip 3pt
\data{1950--51}{Proctor Fellow, Princeton University}
\data{1951--53}{Higgins Research Instructor in Mathematics, Princeton University}
\data{9/1953--1/1955}{Acting Assistant Professor of Mathematics,
Stanford University}
\data{2/1955--6/1958}{Assistant Professor of Mathematics, Dartmouth College}
\data{1958--1961}{Assistant Professor of Communication Science,
M.I.T.}
\data{1961--1962}{Associate Professor of Communication Science, M.I.T.}
\data{1962--present}{Professor of Computer Science,
Stanford University}
\data{1965--1980}{Director, Artificial Intelligence Laboratory,
Stanford University}
\vskip 15pt
\noindent Professional Responsibilities and Scientific Interests:
\vskip 3pt
\data{\hfill$\bullet$\hfill}{With Marvin Minsky organized and directed the Artificial
Intelligence Project at M.I.T.}
\data{\hfill$\bullet$\hfill}{Organized and directs Stanford Artificial Intelligence Laboratory}
\data{\hfill$\bullet$\hfill}{Developed the LISP programming system for
computing with
symbolic expressions, participated in the development
of the ALGOL 58 and the ALGOL 60 languages. Present
scientific work is in the fields of Artificial
Intelligence, Computation with Symbolic Expressions,
Mathematical Theory of Computation, Time-Sharing computer
systems.}
\nextpage
\biblio
\bib{1}{``Projection Operators and Partial Differential
Equations,'' Ph.D.\ Thesis, Princeton University, 1951.}
\bib{2}{``A Method for the Calculation of Limit Cycles by
Successive Approximation'' in Contributions to the Theory of Nonlinear
Oscillations II, Annals of Mathematics Study No.\ 29, Princeton University,
1952, pp.\ 75--79.}
%3McCarthy, John (1953)%1:
\bib{3}{``An Everywhere Continuous Nowhere Differentiable
Function,'' American Mathematical Monthly, December 1953, p.\ 709.}
%3McCarthy, John (1954)%1:
\bib{4}{``A Nuclear Reactor for Rockets,'' Jet Propulsion,
January 1954.}
%3McCarthy, John (1955)%1:
\bib{5}{``The Stability of Invariant Manifolds,'' Applied
Mathematics Laboratory Technical Report No.\ 36, Stanford University, 1955,
p.\ 25.}
%3McCarthy, John (1956)%1:
\bib{6}{``The Inversion of Functions Defined by Turing
Machines,'' in Automata Studies, Annals of Mathematical Study No.\ 34,
Princeton, 1956, pp.\ 177--181.}
%3McCarthy, John (1956)%1:
\bib{7}{``Aggregation in the Open Leontief Model,''
in Progress Report of Dartmouth Mathematics Project, 1956.}
%3McCarthy, John (1956)%1:
\bib{8}{``Measures of the Value of Information,''
National Academy of Science, September 1956.}
%3McCarthy, John (1956)%1:
\bib{9}{Co-editor with Dr. Claude E. Shannon of Automata
Studies, Annals of Mathematics Study No.\ 34., 1956.}
%3McCarthy, John (1960)%1:
\bib{10}{``Recursive Functions of Symbolic Expressions and their
Computation by Machine,'' Comm.\ ACM, April 1960.}
%3McCarthy, John (1960)%1:
\bib{11}{``Programs with Common Sense,'' Proceedings of the
Teddington Conference on the Mechanization of Thought Processes, Her Majesty's
Stationery Office, London, 1960.}
%3McCarthy, John (with 12 others) (1960)%1
\bib{12}{``ALGOL 60'', Numerische
Mathematik, March 1960, also in Comm.\ ACM, May 1960 and Jan.\ 1963.}
%3McCarthy, John (1961)%1:
\bib{13}{``A Basis for Mathematical Theory of Computation,''
in Proc.\ Western Joint Computer Conf., May 1961, pp.\ 225--238.
Later version in Braffort, P. and D. Hirschberg (eds.) Computer
Programming and Formal Systems, North-Holland Publishing Co., 1963.}
%3McCarthy, John (1962)%1:
\bib{14}{``Time-Sharing Computing Systems,'' in Management
and the Computer of the Future, Martin Greenberger (ed.), MIT Press., 1962.}
%3McCarthy, John
\bib{15}{LISP 1.5 Programmer's Manual,
(with Paul Abrahams, Daniel Edwards, Timothy
Hart and Michael Levin),
M.I.T. Press, Cambridge, MA, 1962.}
%3McCarthy, John (1962)%1:
\bib{16}{``Computer Programs for Checking Mathematical Proofs,''
Amer.\ Math.\ Soc.\ Proc.\ of Symposia in Pure Math., vol.\ 5, 1962.}
%3McCarthy, John (1963)%1:
\bib{17}{``Towards a Mathematical Theory of Computation,''
in Proc.\ IFIP Congress 62, North-Holland, Amsterdam, 1963.}
%3McCarthy, John (1963)%1:
\bib{18}{``A Basis for a Mathematical Theory of Computation,''
in P. Braffort and D. Hirschberg (eds.), Computer Programming and
Formal Systems, North-Holland, Amsterdam, 1963, pp.\ 33--70.}
%3McCarthy, John (1963)%1:
\bib{19}{``A Time-Sharing Debugging System for a Small
Computer,'' (with Boilen, Fredkin and Licklider), Proc.\ AFIPS 1963 Spring
Joint Computer Conf., Sparten Books, Detroit, 1963, pp.\ 51--57.}
%3McCarthy, John (1963)%1:
\bib{20}{``The Linking Segment Subprogram Language and
Linking Loader Programming Languages,''
(with F.
Corbato and M. Daggett), Comm.\ ACM, July 1963.}
%3McCarthy, John (1965)%1:
\bib{21}{``Problems in the Theory of Computation,''
in Proc.\ IFIP Congress 65, Spartan, Washington, D.C., 1965.}
\nextpage
%3McCarthy, John (1966)%1:
\bib{22}{``A Formal Description of a Subset of Algol,''
Formal Language Description Languages for Computer Programming,
T.B. Steel, Jr.\ (ed.), North-Holland, Amsterdam, 1966, pp.\ 1--12.}
%3McCarthy, John (1968%1:
\bib{23}{``Time-Sharing Computer Systems,'' in
Conversational Computers, William Orr (ed.), Wiley Publishing Company, 1968.}
%3McCarthy, John (1966)%1:
\bib{24}{``Information,'' Scientific American, vol.\ 215, 1966.}
%3McCarthy, John (1967)%1:
\bib{25}{``THOR---A Display Based Time-Sharing System,''
(with D. Brian, G. Feldman, and John Allen),
AFIPS Conf.\ Proc., vol.\ 30, (FJCC) Thompson, Washington, D.C., 1967.}
%3McCarthy, John (1967)%1:
\bib{26}{``Computer Control of a Hand and Eye,'' in
Proc.\ Third All-Union Conference on Automatic Control (Technical Cybernetics),
Nauka, Moscow, (Russian), 1967.}
%3McCarthy, John (1968)%1:
\bib{27}{``Programs with Common Sense,'' in M. Minsky (ed.),
Semantic Information Processing, M.I.T. Press, Cambridge, MA, 1968.}
%3McCarthy, John (1968)%1:
\bib{28}{``A Computer with Hands, Eyes, and Ears,''
(with L. Earnest, D. Reddy, P. Vicens),
Proc.\ AFIPS Conf.\ (FJCC), 1968.}
%3McCarthy, John and P.J. Hayes (1969)%1:
\bib{29}{``Some Philosophical Problems from
the Standpoint of Artificial Intelligence,'' with P. J. Hayes,
in D. Michie (ed.), Machine
Intelligence 4, American Elsevier, New York, NY, 1969.}
%3McCarthy, John (1972)%1:
\bib{30}{``The Home Information Terminal,'' Man and Computer,
in Proceedings International Conference, Bordeaux 1970, S. Karger, NY, 1972.}
%3McCarthy, John (1973)%1:
\bib{31}{``Mechanical Servants for Mankind,'' in Britannica
Yearbook of Science and the Future, 1973.}
%3McCarthy, John (1974)%1:
\bib{32}{Book Review: ``Artificial Intelligence: A General Survey,''
by Sir James Lighthill, in Artificial Intelligence, vol.\ 5, No.\ 3, 1974.}
%3McCarthy, John (1974)%1:
\bib{33}{``Modeling Our Minds'' in Science Year 1975, The
World Book Science Annual, Field Enterprises Educational Corporation,
Chicago, IL, 1974.}
%3McCarthy, John (1976)%1:
\bib{34}{``The Home Information Terminal,'' invited presentation,
AAAS Annual Meeting, Boston, Feb.\ 18--24, 1976.}
%3McCarthy, John (1976)%1:
\bib{35}{``An Unreasonable Book,'' a review of Computer
Power and Human Reason, by Joseph Weizenbaum (W.H. Freeman and Co., San
Francisco, 1976) in SIGART Newsletter 58, June 1976, also in Creative
Computing, Chestnut Hill, Massachusetts, 1976 and in ``Three Reviews of Joseph
Weizenbaum's Computer Power and Human Reason,'' (with Bruce
Buchanan and Joshua
Lederberg), Stanford Artificial Intelligence Laboratory Memo 291, Computer
Science Department, Stanford, CA, 1976.}
%3McCarthy, John (1977)%1:
\bib{36}{Review: ``Computer Power and Human Reason,'' by Joseph Weizenbaum (W.H.
Freeman and Co., San Francisco, 1976) in Physics Today, 1977.}
%3McCarthy, John (1977)%1:
\bib{37}{``The Home Information Terminal,'' Grolier Encyclopedia, 1977.}
%3McCarthy, John (1977)%1:
\bib{38}{``On The Model Theory of Knowledge,''
(with M. Sato, S. Igarashi, and
T. Hayashi), Proceedings of the Fifth International Joint Conference
on Artificial Intelligence, M.I.T., Cambridge, MA, 1977.}
%3McCarthy, John (1977)%1:
\bib{39}{``Another SAMEFRINGE,'' in SIGART Newsletter No.\ 61, February 1977.}
%3McCarthy, John (1977)%1:
\bib{40}{``History of LISP,'' in Proceedings of the ACM Conference on the
History of Programming Languages, Los Angeles, 1977.}
%3McCarthy, John (1977)%1:
\bib{41}{``Epistemological Problems of Artificial Intelligence,'' Proceedings
of the Fifth International Joint Conference on Artificial
Intelligence, M.I.T., Cambridge, MA, 1977.}
%3McCarthy, John (1979)%1:
\bib{42}{``Ascribing Mental Qualities to Machines,'' in
Philosophical Perspectives
in Artificial Intelligence, Ringle, Martin (ed.), Harvester Press, July 1979.}
%.<<aim 326, MENTAL[F76,JMC]>>
%3McCarthy, John (1979)%1:
\bib{43}{``First Order Theories of Individual Concepts and Propositions,''
in Michie, Donald (ed.) Machine Intelligence 9, University of
Edinburgh Press, Edinburgh, 1979.}
%.<<aim 325,concep[e76,jmc]>>
%3Cartwright, Robert and John McCarthy (1979)%1:
\bib{44}{``Recursive Programs as Functions in a First Order Theory,''
in Proceedings of the International Conference on Mathematical Studies of
Information Processing, Kyoto, Japan, 1979.}
%.<<aim 324, FIRST.NEW[W77,JMC]>>
%3McCarthy, John (1980)%1:
\bib{45}{``Circumscription---A Form of Non-Monotonic Reasoning,''
Artificial Intelligence, vol.\ 13, No.\ 1,2, April 1980.}
%.<<aim 334, circum.new[s79,jmc]>>
%3McCarthy, John and Carolyn Talcott (1980)%1:
\bib{46}{``LISP---Programming and Proving,'' (with Carolyn Talcott),
course notes, Stanford University, (to be published as a book).}
%.<<The references in this bibliography (BIOJMC[1,JMC]) should be in a
%.uniform style, because I often copy them to papers. The last few are
%.correct. The publication in italics and first names spelled out.
%.>>
%3McCarthy, John (1982)%1:
\bib{47}{``Common Business Communication Language,''
Textverarbeitung und\linebreak
B\"urosysteme, Albert Endres and J\"urgen Reetz (eds.),
R. Oldenbourg Verlag, Munich and Vienna, 1982.}
%3McCarthy, John (1983)%1:
\bib{48}{``AI Needs more Emphasis on Basic Research,'' AI
Magazine, vol.\ 4, No.\ 4, Winter 1983.}
\nextpage
\title{Biography of Feferman}
\vskip 12pt
\data{Born:}{December 13, 1928}
\vskip 12pt
\noindent Educational Record:
\data{1948}{B.S., California Institute of Technology}
\data{1957}{Ph.D., University of California, Berkeley}
\vskip 12pt
\noindent Professional Record:
\data{1956--58}{Instructor of Mathematics $\&$ Philosophy, Stanford University}
\data{1958--62}{Assistant Professor of Mathematics $\&$ Philosophy, Stanford University}
\data{1959--60}{National Science Foundation Postdoctoral Fellow, Institute for
Advanced Study}
\data{1958--63}{Consultant, Stanford Research Institute}
\data{1962--68}{Associate Professor of Mathematics $\&$ Philosophy, Stanford
University}
\data{1964--65}{National Science Foundation Senior Postdoctoral Fellow,
University of Paris and University of Amsterdam}
\data{1967--68}{Visiting Associate Professor, Massachusetts Institute of
Technology}
\data{1968--present}{Professor of Mathematics $\&$ Philosophy, Stanford University}
\data{1971--72}{Guggenheim Fellow, University of Oxford and University of Paris}
\data{1979--80}{Visiting Fellow, All Souls and Wolfson Colleges, University
of\linebreak
Oxford}
\data{1980--82}{President, Association for Symbolic Logic}
\biblio
\bib{1}{``The first order properties of products of algebraic systems,''
(with R.\ L.\ Vaught), Fundamenta Mathematicae, vol.\ 47, 1959,
pp.\ 57--103.}
\bib{2}{``Arithmetization of metamathematics in a general setting,''
Fundamenta\linebreak
Mathematicae, vol.\ 49, 1960, pp.\ 35--92.}
\bib{3}{``$1$-consistency and faithful interpretations,''
(with G. Kreisel and S. Orey),
Arch.\ f.\ math.\ logik, vol.\ 6, 1960, pp.\ 52--63.}
\bib{4}{``Classifications of recursive functions by means of hierarchies,''
Trans.\linebreak
Amer.\ Math.\ Soc., vol.\ 104, 1962, pp.\ 101--122.}
\bib{5}{``Transfinite recursive progressions of axiomatic theories,''
J.\ Symbolic\linebreak
Logic, vol.\ 27, 1962, pp.\ 259--316.}
\bib{6}{``Incompleteness along paths in progressions of theories,''
(with C. Spector), J.\ Symbolic Logic, vol.\ 27, 1962, pp.\ 383--390.}
\bib{7}{``Systems of predicative analysis,''
J.\ Symbolic Logic, vol.\ 29, 1964, pp.\ 1--30.}
\bib{8}{``Some applications of the notions of forcing and generic sets,''
(Summary), Proceedings of the International Symposium on the
Theory of Models, Berkeley, June--July 1963, Amsterdam, 1965,
pp.\ 89--95.}
\bib{9}{``Some applications of the notions of forcing and generic sets,''
Fund.\ Math., vol.\ 56, 1965, pp.\ 325--345.}
\bib{10}{``Persistent and invariant formulas relative to theories of higher
order,'' (with G. Kreisel), (Research Announcement), Bull.\ Amer.\ Math.\ Soc.,
vol.\ 72, 1966, pp.\ 480--485.}
\bib{11}{``Predicative provability in set theory,'' (Research Announcement),
Bull.\linebreak
Amer.\ Math.\ Soc., vol.\ 72, 1966, pp.\ 486--489.}
\bib{12}{``Systems of predicative analysis, II: representations of ordinals,''
J.\ of Symbolic Logic, vol.\ 33, 1968, pp.\ 193--220.}
\bib{13}{``Autonomous transfinite progressions and the extent of predicative
mathematics,'' pp.\ 121--135 in: Logic, Methodology and Philosophy
of Science, III, ed.\ v.\ Rootselaar and Staal, Amsterdam, 1968.}
\bib{14}{``Persistent and invariant formulas for outer extensions,''
Compos.\ Math., vol.\ 20, 1968, pp.\ 29--52.}
\bib{15}{``Lectures on proof theory,'' pp.\ 1--107 in Lecture Notes in Mathematics,
vol.\ 70, 1968, pp.\ 29--52.}
\bib{16}{``Hereditarily replete functionals over the ordinals,'' in Intuitionism
and Proof Theory, ed. Myhill, Kino, Versley, Amsterdam, 1970,
pp.\ 289--301.}
\bib{17}{``Formal theories for transfinite iterations of generalized inductive
definitions and some subsystems of analysis,'' {\it ibid.}, pp.\ 303--326.}
\bib{18}{``Ordinals associated with theories for one inductively defined set,''
(preliminary version prepared).}
\bib{19}{``Set-theoretical foundations of category theory,'' (with an Appendix
by G. Kreisel) pp.\ 201--247, Report of the Midwest Category
Seminar, III,\linebreak
Springer Lecture Notes in Mathematics, vol.\ 106, 1969.}
\bib{20}{``Predicatively reducible systems of set theory,'' pp.\ 11--32 in
Axiomatic Set Theory (Proc.\ Symp.\ Pure Math.\ XIII, Part II),
A.M.S., 1974.}
\bib{21}{``Ordinals and functionals in proof theory,'' Proc.\ Intl.\ Cong.\ Math.,
Nice, 1970, vol.\ 1, pp.\ 229--233.}
\bib{22}{``Infinitary properties, local functors, and systems of ordinal
functions,'' Proc.\ Bedford College Conf.\ on Math.\ Logic,
Londond 1970, ed., W.\linebreak
Hodges, Springer Lecture Notes, 255, 1972,
pp.\ 63--97.}
\bib{23}{``Applications of many-sorted interpolation theorems,''
Proc.\ of the Tarski Symposium, 1974, 205--223.}
\bib{24}{``Two notes on abstract model theory. I. Properties invariant
on the range of definable relations between structures,''
Fund.\ Math.\ 82, 1974, pp.\ 153--165.}
\bib{25}{``Two notes on abstract model theory, II. Languages for which the set
of valid sentences is semi-invariantly implicitly definable,''
Fund.\ Math., 89, 1975, pp.\ 111--130.}
\bib{26}{``Recursion in total functionals of finite type,'' Compositio
Math., 35, 1977, pp.\ 3--22.}
\bib{27}{``A language and axioms for explicit mathematics,'' in Algebra and Logic,
ed., Crossley, Springer Lecture Notes, 450, 1975, pp.\ 87--139.}
\bib{28}{``A more perspicuous formal system for predicativity,'' in
Konstruktionen vs.\ Positionen I, Walter de Gruyter, Berlin, 1978, pp.\ 68--93.}
\bib{29}{``Impredicativity of the existence of the largest divisible subgroup of
an Abelian $p$-group . Model Theory and Algebra,'' (A memorial tribute to
A. Robinson), Lecture Notes in Mathematics, 498, 1975, pp.\ 117--130.}
\bib{30}{``Non-extensional type-free theories of partial operations and
classifications,
I,'' Proof Theory Symposium, Kiel, 1974, Springer Lecture Notes in Mathematics,
500, 1975, pp.\ 73--118.}
\bib{31}{``Generating schemes for partial recursively continuous functionals,''
(summary), pp.\ 191--198 in Colloque International de Logique,
(Clermont-\linebreak
Ferrand 1975), CNRS, 1977.}
\bib{32}{``Theories of finite type related to mathematical practice,''
pp.\ 913--971
in Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977.}
\bib{33}{``Categorical foundations and foundations of category theory,''
pp.\ 149--169
in Logic, Foundations of Mathematics and Computability Theory,
(Proc.\ 5th Int.\ Congr.\ Logic, Methodology, and Philosophy of
Science, London, Ont., Part I), D. Reidel, Dordrecht, 1977.}
\bib{34}{``Generalizing set-theoretical model theory and an analogue theory
on admissible sets,'' in Essays on mathematical and philosophical logic,
(Proc.\ 4th Scandinavian Logic Sympos.), Reidel, Dordrecht, 1978,
pp.\ 171--195.}
\bib{35}{``Review of Proof Theory'' by G. Takeuti, Bull.\ Amer.\ Math.\ Soc., 83,
1977, pp.\ 351--361.}
\bib{36}{``Inductive schemata and recursively continuous functionals,''
pp.\ 373--392
in Logic Colloquium 76 (Proc.\ Oxford Conf.), North-Holland,
Amsterdam, 1977.}
\bib{37}{``Recursion theory and set theory: a marriage of convenience,''
pp.\ 55--98
in Proc.\ of Generalized Recursion theory Symposium II (Oslo, Norway,
1977), North-Holland, Amsterdam, 1978.}
\bib{38}{``Review of Proof Theory by K. Sch\"utte,'' Bull.\ (New Series)
Amer.\ Math.\ Soc., 1, 1979, pp.\ 224--228.}
\bib{39}{``What does logic have to tell us about mathematical proofs?''
The Mathematical Intelligencer, 2, 1979, pp.\ 20--24.}
\bib{40}{``Constructive theories of functions and classes,'' pp.\ 159--224 in
Logic Coloquium 78 (Proc.\ Mons Conf.), North-Holland, Amsterdam, 1979.}
\bib{41}{``Consistency of the unrestricted abstraction principle using an
intensional equivalence operator,'' (with P. Aczel), pp.\ 67--98 in
To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and
Formalism, Academic Press, New York, 1980.}
\bib{42}{``Iterated inductive definitions and subsystems of analysis: recent
proof-theoretical studies,'' (With W. Buchholz, W. Pohlers, and W. Sieg),\linebreak
Springer Lecture Notes in Math., 897, 1981, p.\ 338 Introduction
by S. Fefermn, pp.\ 1--15.}
\bib{43}{``Iterated inductive definitions and subsystems of analysis,''
(with W. Sieg), Ch.\ I,
{\it ibid.}, 897, 1981, pp.\ 16--77.}
\bib{44}{``Proof-theoretic equivalences between classical and constructive
theories
for analysis,'' (with W. Sieg), Ch.\ II, {\sl ibid.}, 897, 1981,
pp.\ 78--142.}
\bib{45}{``Iterated inductive fixed-point theories: Applications to Hancock's
conjecture,'' in Patras Logic Symposion, North-Holland, 1982, pp.\ 171--196.}
\bib{46}{``Inductively presented systems and the formalization of
meta-mathe-\linebreak
matics,'' in Logic Colloquium '80, North-Holland, 1982,
pp.\ 95--182.}
\bib{47}{``Monotone inductive definitions,'' in The L. E. J. Brouwer Centenary
Symposium, North-Holland, 1982, 77--89.}
\bib{48}{``Choice principles, the bar rule and autonomously iterated comprehension
schemes in analysis,'' (with G. J\"ager), J.\ Symbolic Logic 48, 1983,
pp.\ 63--70.}
\bib{49}{``A theory of variable types,'' to appear in Proc.\ VIth Latin American
Logic Symposium, 1981.}
\bib{50}{``Toward useful type-free theories,'' I, to appear in J.\ Symbolic
Logic.}
\bib{51}{``Conviction and caution: A scientific portrait of Kurt G\"odel,''
contributed paper for 7th International Congress for Logic, Methodology
and Philosophy of Science, Salzburg, 11--16 July 1983.}
\bib{52}{``Working foundations,'' to appear in Proc.\ of the Workshop on the
``Present state of the problem of foundations of mathematics,''
Florence, 15--19 June 1981.}
\bib{53}{``Foundational ways,'' to appear in Oberwolfach Dokumentations-Band.}
\bib{54}{``Between constructive and classical mathematics,'' to appear
in Logic Colloquium '83 (Proc.\ Aachen Conference).}
\bib{55}{``Intensionality in mathematics,'' to appear in Proc.\ Pacific
division APA, Spring '84 meeting.}
\nextpage
\title{Biography of Goad}
\vskip 12pt
\data{Born:}{October 27, 1953 in Los Alamos, NM}
\vskip 12pt
\noindent Education:
\data{1974}{B.A., (Mathematics) Cornell University, Ithaca, N.Y.}
\data{1980}{Ph.D., (Computer Science) Stanford University, Stanford, CA}
\vskip 12pt
\noindent Professional Experience:
\data{8/1983--present}{President, Silma Incorporated (on leave from Stanford
University)}
\data{1980--present}{Research Associate,
Computer Science Department, Stanford University}
\data{1974--75}{Staff Member, Los Alamos Scientific Laboratory}
\biblio
\bib{1}{``Special purpose automatic programming for 3D model-based vision,''
Proceedings of the Sixth ARPA Workshop on Image Understanding, June 1983.}
\bib{2}{``Automatic construction of
special purpose programs for hidden surface elimination,''
Proceedings of the Ninth Annual Conference on Computer Graphics and
Interactive Techniques (SIGGRAPH), Boston, MA, July\linebreak
1982.}
\bib{3}{``Automatic construction of special purpose programs,''
Proceedings of the Sixth Conference on Automated Deduction, New York,
NY, June 1982.}
\bib{4}{``Computational uses of the manipulation of formal proofs,'' (Thesis),
Stanford University Computer Science Department Report STAN-CS-80-819, August
1980.}
\bib{5}{``Proofs as descriptions of computation,''
Proceedings of the Fifth Conference on Automated Deduction, Les Arcs, France,
July 1980.}
\bib{6}{``Monadic infinitary propositional logic: a special operator,''
Reports on Mathematical Logic, 10, 1978, pp.\ 43--53.}
\bib{7}{``A clustering algorithm for mixtures of monotone densities,''
Los Alamos Scientific Laboratory Report LA-7120-MS, January 1978.}
\bib{8}{``A MUMPS code-building package for data base management,''
Los Alamos Scientific Laboratory Report LA-6165-MS, September 1975.}
\bib{9}{``A flow-system multiangle light scattering instrument for cell
characterization,'' (with G. C. Salzman, J. M. Crowell et al), Clinical
Chemistry, vol.\ 21, 1297, 1975.}
\nextpage
\title{Biography of Ketonen}
\data{Born:}{April 3, 1952 in Helsinki, Finland}
\vskip 12pt
\noindent Education:
\data{1968}{B.A., M.A. (Mathematics) {\AA}bo Akademi, Turku, Finland}
\data{1971}{Ph.D. (Mathematics) University of Wisconsin, Madison}
\vskip 12pt
\noindent Honors and Fellowships:
\data{1968--71}{Fulbright Travel Grant}
\data{1968--71}{University of Wisconsin Fellowship}
\data{1971--72}{George William Hill Research Instructorship}
\data{1972--74}{Miller Fellowship}
\vskip 12pt
\noindent Professional Experience:
\data{1983--present}{Senior Research Associate,
Computer Science Department, Stanford University}
\data{1979--83}{Research Associate,
Computer Science Department
(jointly with the Institute for Mathematical
Studies for Social Sciences, 1979--81)}
\data{1983}{Consultant, Silma}
\data{1981}{Consultant, PERSEUS and Hewlett-Packard}
\data{1977--79}{Visiting Associate Professor,
Department of Mathematics, Stanford University}
\data{1975--80}{Associate Professor,
Department of Mathematics, University of Hawaii}
\data{1974--75}{Research Associate,
Department of Mathematics, University of\linebreak
California at Berkeley}
\data{1972--74}{Miller Fellow, University of California at Berkeley}
\data{1971--72}{George William Hill Research Instructor,
Department of Mathematics, State University of New York at Buffalo}
\biblio
\bib{1}{``Everything you wanted to know about ultrafilters,''
Doctoral dissertation, University of Wisconsin, 1971.}
\bib{2}{``On non-regular ultrafilters,'' Journal of Symbolic Logic 37,
1972, pp.\ 71--74.}
\bib{3}{``Strong compactness and other cardinal sins,'' Annals of Mathematical
Logic 5, 1972, pp.\ 47--76.}
\bib{4}{``Ultrafilters over measurable cardinals,'' Fundamenta Mathematicae 77,
1973, pp.\ 257--269.}
\bib{5}{``On Almost Disjoint Sets,'' Notices American Mathematical Society 21,
1974, p.\ 557.}
\bib{6}{``Some combinatorial principles,'' Transactions of the American
Mathematical Society 188, 1974, pp.\ 387--394.}
\bib{7}{``Banach spaces and large cardinals,'' Fundamenta Mathematicae 81,
1974, pp.\ 291--303.}
\bib{8}{``On regularity of ultrafilters,'' Israel Journal of Mathematics 17,
1974, pp.\ 231--240.}
\bib{9}{``On the existence of P-points,'' Fundamenta Mathematicae 92,
1976, pp.\ 91--94.}
\bib{10}{``Non-regular ultrafilters and large cardinals,'' Transactions of the
American Mathematical Society 224, 1976, pp.\ 61--73.}
\bib{11}{``The structure of countable Boolean algebras,'' Annals of Mathematics
108, 1978, p.\ 41--89.}
\bib{12}{``Open problems in the theory of ultrafilters,'' Proceedings of the
Fourth Scandinavian Logic Conference in Jyv\"askyl\"a, edited
by K.J.J.Hintikka, I.Niiniluoto and E.Saarinen.
(D.Reidel), 1979, pp.\ 227--247.}
\bib{13}{``On finitely axiomatizable theories,'' accepted for
Proceedings of the American Mathematical Society, 1979, 12pp.}
\bib{14}{``Isomorphism types of countable Boolean algebras,'' notes
in circulation, 1979, 42pp.}
\bib{15}{``Some combinatorial properties of ultrafilters,'' Fundamenta
Mathematicae 1070, 1980, pp.\ 225--235.}
\bib{16}{``Rapidly growing Ramsey functions,'' Annals of Mathematics 113,
1981, pp.\ 267--314.}
\bib{17}{``Efficient theorem proving in set theory,''
in University-Level Computer-Assisted Instruction at
Stanford: 1968--1980, Edited by Patrick Suppes, IMSSS, Stanford, 1981,
pp.\ 121--126.}
\bib{18}{``On a decidable fragment of predicate calculus,''
in University-Level Com\-puter-Assisted Instruction at
Stanford: 1968--1980, Edited by Patrick Suppes,
IMSSS, Stanford, 1981, pp.\ 127--131.}
\bib{19}{``Deducing Facts about Scenes from Images,''
in Proceedings of the Image Understanding Workshop, 1983, pp.\ 182--183.}
\bib{20}{``The Language of an Interactive Proof Checker,''
34 pp., Stanford University, CS Report STAN-CS-83-992, 1983.}
\bib{21}{``A Decidable Fragment of Predicate Calculus,''
accepted for publication in the Journal for Theoretical Computer Science,
1984, 20 pp.}
\bib{22}{``EKL---A Mathematically Oriented Proof Checker,''
20 pp., Stanford University. Accepted for the Proceedings of the Seventh
Conference on Automated Deduction, 1984.}
\bib{23}{``EKL---An interactive proof checker,''
User's Reference Manual, 50 pp., Stanford University, 1983.}
\bib{24}{``A Type System for a Mechanized Logic,''
25 pp., Stanford University, 1983.}
\nextpage
\title{Biography of Talcott}
\data{Born:}{June 14, 1941 in Caldwell, Idaho}
\vskip 12pt
\noindent Education:
\data{1962}{B.S. (Chemistry) University of Denver, Denver, Colorado}
\data{1966}{Ph.D. (Chemistry) University of California at Berkeley, California}
\vskip 12pt
\noindent Fellowships and Societies:
\data{1958}{National Honor Society}
\data{1962}{Phi Beta Kapa}
\data{1968--69}{NSF Postdoctoral Fellowship}
\data{1978--79}{IBM Graduate Fellowship}
\data{}{Association for Symbolic Logic}
\vskip 12pt
\noindent Professional Experience
\data{1977--present}{Research Assistant, the Stanford Artificial Intelligence
Laboratory, Stanford University}
\data{1980--present}{Consultant, PERSEUS}
\data{1979}{IBM Summer Student Visitor,
IBM Watson Research Laboratory}
\data{1969--75}{Research Associate and
Teaching Assistant in Mathematics,
University of California, Santa Cruz}
\data{1968}{PostDoctoral Fellowship,
Computer applications to theoretical\linebreak
chemistry, Cambridge Universtiy, England}
\data{1964--66}{Research Assistant, University of California at Berkeley}
\data{1973--75}{Laboratory Assistant in Analyitcal Chemistry,
Denver Research Institute}
\biblio
\hbox to\hsize{\hskip 3pc (Note---some publications as C.T. Williamson.)\hfill}
\vskip 6pt
\bib{1}{``The Cyclononatetraene Anion Radical,''
(with Katz,T.J.), J.\ Am.\ Chem.\ Soc.\ 88, 1966, p.\ 4732.}
\bib{2}{``Electron Spin Resonance of the Radical Anions of Pyridine
and Related Nitrogen Heterocyclics,''
(with Meyers,R.J.),
Mol.\ Phys.\ 12, 1967, pp.\ 549--567.}
\bib{3}{``Electron Spin Resonance Studies of Radicals Produced by Electrolysis,''
Ph.D.\ Thesis, University of California at Berkeley, 1967.}
\bib{4}{``The Double Bond in Ethylene,''
(with Amaral, A.M.S.C., Linnett, J.W. (as Williamson, C.T.)),
Theoret.\ Chim.\ Acta(Berlin) 16, 1970,
pp.\ 249--262.}
\bib{5}{``Some Computations Involving Simple Lie Algebras,''
(with Burgoyne, N., (as Williamson, C.T.)),
in {\sl Proceedings of the Second ACM Symposium on Symbolic and Algebraic
Manipulation}, March 1971, pp.\ 162--171.}
\bib{6}{``Algorithm Verification Applied to the Todd-Coxeter Algorithm,''
(with Maurer, W. D., (as Williamson, C.T.)),
Electronics Research Lab., College of Engineering, U.C. Berkeley, Memorandum
ERL-M317, December 1971.}
\bib{7}{``On a theorem of Borel and Tits for Finite Chevalley Groups,''
(with Burgoyne, N. (as Williamson, C.T.)), 1976.}
\bib{8}{``Semi-simple Classes in Chevalley Type Groups,''
(with Burgoyne, N. (as Williamson, C.T.)),
Pacific Journal of Mathematics, 70, 1977, p.\ 83--100.}
\bib{9}{``LISP---Programming and Proving,''
(with McCarthy, John),
course notes, Stanford University, (to be published as a book).}
\nextpage
\title{Biography of Weyhrauch}
\data{Born:}{July 3, 1943, Blue Point, New York}
\vskip 12pt
\noindent Education:
\data{1975}{Ph.D. (Mathematics) Stanford University}
\data{1966}{M.S. (Mathematics) Stanford University}
\data{1965}{B.A. (Mathematics) New York University}
\vskip 12pt
\noindent Professional Experience:
\data{1971--6/1980}{Research Associate, Artificial Intelligence Lab, Stanford
University}
\data{6/1980--2/1981}{Director of a LISP development project as part
of
a joint venture between Hewlett-Packard and {PERSEUS} (California
corporation).}
\data{2/1981--present}{Research Associate, Computer Science Department, Stanford
University}
\biblio
\bib{1}{``Program Semantics and Correctness in a Mechanized Logic,''
(with Milner, R.),
Proceedings of the USA-Japan Computer Conference, Tokyo, 1972.}
\bib{2}{``Proving Compiler Correctness in a Mechanized Logic,''
(with Milner, R.),
Machine Intelligence 7, Edinburgh
University Press, 1972.}
\bib{3}{``AFTER LEIBNIZ$\ldots$: Discussions on Philosophy and Artificial
Intelligence,''
(with Anderson, D.B., Binford, T.O., Thomas, A.J., and Wilks, Y.A.),
Stanford Artificial Intelligence Laboratory Memo AIM-229, Stanford University,
April 1974.}
\bib{4}{``LCFsmall: an Implementation of LCF,''
(with Aiello, L.),
Stanford Artificial Intelligence Laboratory Memo AIM-241, Stanford University,
August 1974.}
\bib{5}{``Checking Proofs in the Metamathematics of First Order Logic,''
(with Aiello, M.),
Stanford Artificial Intelligence Laboratory Memo AIM-222, Stanford University,
August 1974.}
\bib{6}{``FOL: A Proof Checker for First-order Logic,''
(with Thomas, A.),
Stanford Artificial Intelligence Laboratory Memo AIM-235, Stanford University,
September 1974.}
\bib{7}{``The Semantics of PASCAL in LCF,''
(with Aiello, L., and Aiello, M.),
Stanford Artificial Intelligence Laboratory Memo AIM-221, Stanford University,
October 1974.}
\bib{8}{``Another Axiomatization of PASCAL, or Why axiomatize programming
languages,''
(with Aiello, L., and Aiello, M.),
Nota Interna IEI B-74-42, 1974.}
\bib{9}{``Properties of programming languages used in the LCF verification of
programs,''
(with Aiello, L., and Aiello, M.),
Nota Scientifica ISI S-75-3, Universit\`a di Pisa, 1974.}
\bib{10}{``Relations Between Some Hierarchies of Ordinal Functions
and Functionals,''
Ph.D.\ Dissertation, Stanford University, Stanford, CA, November 1975.}
\bib{11}{``Practical program verification: are we close,''
Calcolo, Suppleemento N.\ 1, vol.\ XII, Proceedings of a meeting on 20 years of
computer science, Pisa, June 16--19, 1975.}
\nextpage
\bib{12}{``Checking Proofs in the Metamathematics of First Order Logic,''
(with Aiello, M.),
Advance papers of the Fourth International joint conference on Artificial
Intelligence, Tblisi, Georgia, USSR, September 1975.}
\bib{13}{``An FOL Primer,''
(with Filman, R.),
Stanford Artificial Intelligence Laboratory Memo AIM-288, Stanford University,
September 1976.}
\bib{14}{``FOL: A Proof Checker for First-order Logic,''
Stanford Artificial Intelligence Laboratory Memo AIM-235.1, Stanford University,
August 1977.}
\bib{15}{``Pascal in LCF: Semantics and Examples of Proofs,''
(with Aiello, L., and Aiello, M.),
Theoretical Computer Science 5, 1977.}
\bib{16}{``Lecture notes on the use of logic in artificial intelligence
and mathematical
theory of computation,'' Summer school on the foundations of artificial
intelligence and computer science (FAICS), June 1978.}
\bib{17}{``Many Sorted First Order Logic,''
Proceedings of the Fourth Workshop on Automated deduction, February 1979.}
\bib{18}{``Prolegomena to a theory of mechanized formal reasoning,''
Stanford Artificial Intelligence Laboratory Memo AIM-315, Stanford University,
December 1978.}
\bib{19}{``Prolegomena to a theory of mechanized formal reasoning,''
Artificial Intelligence, 13, 1980, p.\ 133--170.}
\bib{20}{``LISP applied to boolean logic,''
(with Graves, H.),
Byte Magazine, August 1979.}
\bib{21}{``Using meta-theoretic reasoning to do algebra,''
(with Aiello, L.),
Procedings of the 5-th
Workshop on Automated Deduction, Springer-Verlag,
Lecture Notes in Computer Science, 1980.}
\bib{22}{``Prolegomena to a theory of mechanized formal reasoning,''
reprinted in ``Readings in Artifical Intelligence'', ed. Bonnie Lynn Webber and
Nils Nilsson, Tioga Publishing, 1981.}
\bib{23}{``An example of FOL using metatheory---Formalizing
reasoning systems and introducing derived inference rules,''
to appear in Proceedings of the 6-th Conference on Automated Deduction,
June 1982.}
\bib{24}{``Reasoning about actions,''
(with Talcott, C.), in preparation.}
\bib{25}{``A Decidable Fragment of Predicate Calculus,''
(with Ketonen, J.),
accepted for publication in the Journal for Theoretical Computer Science,
1984, 20 pp.}
\done